(set-logic BV)

(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

(synth-fun f ( (x (BitVec 64))) (BitVec 64)
(

(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
                    (shl1 Start)
 		    (shr1 Start)
		    (shr4 Start)
		    (shr16 Start)
		    (bvand Start Start)
		    (bvor Start Start)
		    (bvxor Start Start)
		    (bvadd Start Start)
		    (if0 Start Start Start)
 ))
)
)
(constraint (= (f #x0CE1A890FFD1BC81) #x0CEDE9B8FFFFFDBD))
(constraint (= (f #xF443197D724EFFFF) #xF4F75B7D7F7EFFFF))
(constraint (= (f #x5B32B80C4D09D378) #x5B7BBABC4D4DDBFB))
(constraint (= (f #xC76939EB8945E497) #xC7EF79FBEBCDE5F7))
(constraint (= (f #x2AE77F1CF187B935) #x2AEFFF7FFDF7BFBD))
(constraint (= (f #xFFFFFFFFFFFFFFFE) #xFFFFFFFFFFFFFFFF))
(constraint (= (f #xBE3D9EAB43751F47) #xBEBFBFBFEB777F5F))
(constraint (= (f #xA4A9110548290DB3) #xA4ADB9154D692DBF))
(constraint (= (f #x0B2ECDFA63411926) #x0B2FEFFFFB63593F))
(constraint (= (f #x0831557BF4493BF8) #x0839757FFFFD7BFB))
(constraint (= (f #xEA2D762448D336E7) #xEAEF7F766CDBF7F7))
(constraint (= (f #xFB5165A85C4AA604) #xF6A2CB50B8954C0B))
(constraint (= (f #x6470011AEAD6F6F8) #xC8E00235D5ADEDF3))
(constraint (= (f #x495207AE5BA6DE44) #x92A40F5CB74DBC8B))
(constraint (= (f #x5A760CA210AEEAA5) #xB4EC1944215DD54D))
(constraint (= (f #xA1959BFD324BFFFF) #x432B37FA64980001))
(constraint (= (f #x88A63A89ABB42CA0) #x114C751357685943))
(constraint (= (f #x208D44805ED654EB) #x411A8900BDACA9D9))
(constraint (= (f #x5CA460A8CA0A43EE) #xB948C151941487DF))
(constraint (= (f #x7D5627A1CCDA1407) #xFAAC4F4399B42811))
(constraint (= (f #xC14B69A0471A361A) #x8296D3408E346C37))
(constraint (= (f #x00000000000001CE) #x000000000000039D))
(constraint (= (f #x0000000000000177) #x00000000000002EF))
(constraint (= (f #x0000000000000164) #x00000000000002C9))
(constraint (= (f #x0000000000000102) #x0000000000000205))
(check-synth)
